\begin{tabbing}
$\forall$${\it tg}$:Id, $k$:Knd, $l$:IdLnk, $T$, $B$:Type, $f$:($B$$\rightarrow$$T$).
\\[0ex](rcv($l$,${\it tg}$) $=$ $k$ $\Rightarrow$ $T$ $=$ $B$)
\\[0ex]$\Rightarrow$ \=@source($l$): ma{-}single{-}sends0($B$;$T$;$k$;$l$;${\it tg}$;$\lambda$$b$.[$f$($b$)]) $\in$ Dsys\+
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@source($l$): ma{-}single{-}sends0($B$;$T$;$k$;$l$;${\it tg}$;$\lambda$$b$.[$f$($b$)]) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]($\forall$$e$:E. loc($e$) $=$ source($l$) $\in$ Id $\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $B$)
\\[0ex]\& ($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]\& sender(${\it e'}$) $=$ $e$ $\in$ E \& val(${\it e'}$) $=$ $f$(val($e$)) $\in$ $T$)))
\-\-\-\-\-
\end{tabbing}